(set-logic QF_UFLIA)
(set-info :source |
  These benchmarks were obtained from the KIND tool during verification of
  Lustre programs.  See also the lustre family of benchmarks in QF_LIA.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(declare-fun _base () Int)
(declare-fun _n () Int)
(assert (<= 0 _n))
(declare-fun ___z3z___ (Int) Bool)
(declare-fun ___z4z___ (Int) Bool)
(declare-fun ___z5z___ (Int) Bool)
(declare-fun ___z6z___ (Int) Bool)
(declare-fun ___z7z___ (Int) Bool)
(declare-fun ___z8z___ (Int) Int)
(push 1)
(assert (= (= (___z5z___ 0) (___z4z___ 0)) (___z3z___ 0)))
(assert (= (___z4z___ 0) (and (___z7z___ 0) (___z6z___ 0))))
(assert (= (___z5z___ 0) (= (___z8z___ 0) 2)))
(assert (let ((?v_0 (= _base 0))) (= (___z6z___ 0) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 1))))))))
(assert (let ((?v_0 (= _base 0))) (= (___z7z___ 0) (and (not ?v_0) (or ?v_0 (___z6z___ (- 1)))))))
(assert (let ((?v_0 (___z8z___ (- 1)))) (= (___z8z___ 0) (ite (= _base 0) 0 (ite (= ?v_0 3) 0 (+ 1 (+ 1 ?v_0)))))))
(assert (= (= (___z5z___ (- 1)) (___z4z___ (- 1))) (___z3z___ (- 1))))
(assert (= (___z4z___ (- 1)) (and (___z7z___ (- 1)) (___z6z___ (- 1)))))
(assert (= (___z5z___ (- 1)) (= (___z8z___ (- 1)) 2)))
(assert (let ((?v_0 (= _base (- 1)))) (= (___z6z___ (- 1)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 2))))))))
(assert (let ((?v_0 (= _base (- 1)))) (= (___z7z___ (- 1)) (and (not ?v_0) (or ?v_0 (___z6z___ (- 2)))))))
(assert (let ((?v_0 (___z8z___ (- 2)))) (= (___z8z___ (- 1)) (ite (= _base (- 1)) 0 (ite (= ?v_0 3) 0 (+ 1 (+ 1 ?v_0)))))))
(push 1)
(assert (not (or (not (= _base (- 1))) (and (___z3z___ 0) (___z3z___ (- 1))))))
(assert true)
(set-info :status sat)
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
